dfib2(s1(s1(x)), y) -> dfib2(s1(x), dfib2(x, y))
↳ QTRS
↳ DependencyPairsProof
dfib2(s1(s1(x)), y) -> dfib2(s1(x), dfib2(x, y))
DFIB2(s1(s1(x)), y) -> DFIB2(x, y)
DFIB2(s1(s1(x)), y) -> DFIB2(s1(x), dfib2(x, y))
dfib2(s1(s1(x)), y) -> dfib2(s1(x), dfib2(x, y))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ QDPOrderProof
DFIB2(s1(s1(x)), y) -> DFIB2(x, y)
DFIB2(s1(s1(x)), y) -> DFIB2(s1(x), dfib2(x, y))
dfib2(s1(s1(x)), y) -> dfib2(s1(x), dfib2(x, y))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
DFIB2(s1(s1(x)), y) -> DFIB2(x, y)
DFIB2(s1(s1(x)), y) -> DFIB2(s1(x), dfib2(x, y))
POL(DFIB2(x1, x2)) = 3·x1 + 2·x1·x2 + 2·x2
POL(dfib2(x1, x2)) = 2 + 3·x1 + 3·x1·x2
POL(s1(x1)) = 3 + 3·x1 + 2·x12
dfib2(s1(s1(x)), y) -> dfib2(s1(x), dfib2(x, y))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
dfib2(s1(s1(x)), y) -> dfib2(s1(x), dfib2(x, y))